es:event_system{i:l}, e,e':es-E(es). es-ble{i:l}(es;e;e')   

latex

Definitions	x:A. B(x), t  T, es-ble{i:l}(es;e;e'), prop{i:l}, P  Q, decidable(P), P  Q
Lemmas	event system wf, es-E wf, decidable wf, es-le wf, btrue wf, bfalse wf